A, B:Type, f:(AB), L:A List, L1, L2:B List.
map(f;L) = (L1 @ L2)  B List  {map(f;firstn(||L1||;L)) = L1 & map(f;nth_tl(||L1||;L)) = L2} 

latex

Definitions	Unit, P  Q, T, , b, b, True, AB, A, False, hd(l), ij, S  T, Top, tl(l), as @ bs, P  Q, P  Q, P & Q, i<j, Prop, map(f;as), if b t else f fi, ij, ||as||, nth_tl(n;as), {T}, x:A. B(x), t  T
Lemmas	nth tl wf, length wf1, le int wf, ifthenelse wf, map wf, append is nil, append wf, top wf, first0, non neg length, hd wf, tl wf, ge wf, bnot wf, assert wf, le wf, assert of lt int, bnot of le int, eqff to assert, iff transitivity, assert of le int, eqtt to assert, bool wf, lt int wf, bnot of lt int, true wf, squash wf